T:Type, L1, L2, L1', L2':(T List). L1  L1'  L2  L2'  L1 @ L2  L1' @ L2' 

latex

Definitions	t  T, x:A. B(x), L1  L2, P  Q, x:A. B(x), T, ff, P  Q, P  Q, tt, if b then t else f fi , True, P & Q, , i  j < k, {i..j}, increasing(f;k), False, A, A  B, suptype(S; T), S  T, Unit, ,
Lemmas	sublist wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, assert of lt int, eqtt to assert, iff transitivity, bnot wf, le int wf, le wf, length append, append wf, non neg length, int seg wf, assert wf, bool wf, length wf1, lt int wf, select append front, select wf, select append back, increasing wf